Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	eq(0,0)	→ true
2:	eq(0,s(x))	→ false
3:	eq(s(x),0)	→ false
4:	eq(s(x),s(y))	→ eq(x,y)
5:	le(0,y)	→ true
6:	le(s(x),0)	→ false
7:	le(s(x),s(y))	→ le(x,y)
8:	app(nil,y)	→ y
9:	app(add(n,x),y)	→ add(n,app(x,y))
10:	min(add(n,nil))	→ n
11:	min(add(n,add(m,x)))	→ if_min(le(n,m),add(n,add(m,x)))
12:	if_min(true,add(n,add(m,x)))	→ min(add(n,x))
13:	if_min(false,add(n,add(m,x)))	→ min(add(m,x))
14:	rm(n,nil)	→ nil
15:	rm(n,add(m,x))	→ if_rm(eq(n,m),n,add(m,x))
16:	if_rm(true,n,add(m,x))	→ rm(n,x)
17:	if_rm(false,n,add(m,x))	→ add(m,rm(n,x))
18:	minsort(nil,nil)	→ nil
19:	minsort(add(n,x),y)	→ if_minsort(eq(n,min(add(n,x))),add(n,x),y)
20:	if_minsort(true,add(n,x),y)	→ add(n,minsort(app(rm(n,x),y),nil))
21:	if_minsort(false,add(n,x),y)	→ minsort(x,add(n,y))

There are 18 dependency pairs:


22:	EQ(s(x),s(y))	→ EQ(x,y)
23:	LE(s(x),s(y))	→ LE(x,y)
24:	APP(add(n,x),y)	→ APP(x,y)
25:	MIN(add(n,add(m,x)))	→ IF_MIN(le(n,m),add(n,add(m,x)))
26:	MIN(add(n,add(m,x)))	→ LE(n,m)
27:	IF_MIN(true,add(n,add(m,x)))	→ MIN(add(n,x))
28:	IF_MIN(false,add(n,add(m,x)))	→ MIN(add(m,x))
29:	RM(n,add(m,x))	→ IF_RM(eq(n,m),n,add(m,x))
30:	RM(n,add(m,x))	→ EQ(n,m)
31:	IF_RM(true,n,add(m,x))	→ RM(n,x)
32:	IF_RM(false,n,add(m,x))	→ RM(n,x)
33:	MINSORT(add(n,x),y)	→ IF_MINSORT(eq(n,min(add(n,x))),add(n,x),y)
34:	MINSORT(add(n,x),y)	→ EQ(n,min(add(n,x)))
35:	MINSORT(add(n,x),y)	→ MIN(add(n,x))
36:	IF_MINSORT(true,add(n,x),y)	→ MINSORT(app(rm(n,x),y),nil)
37:	IF_MINSORT(true,add(n,x),y)	→ APP(rm(n,x),y)
38:	IF_MINSORT(true,add(n,x),y)	→ RM(n,x)
39:	IF_MINSORT(false,add(n,x),y)	→ MINSORT(x,add(n,y))

The approximated dependency graph contains 6 SCCs: {24}, {22}, {23}, {25,27,28}, {29,31,32} and {33,36,39}.

Consider the SCC {24}. There are no usable rules. By taking the AF π with π(APP) = 1 and π(add) = [2] together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.

Consider the SCC {22}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 22 is strictly decreasing.

Consider the SCC {23}. There are no usable rules. By taking the AF π with π(LE) = 1 together with the lexicographic path order with empty precedence, rule 23 is strictly decreasing.

Consider the SCC {25,27,28}. The usable rules are {5-7}. By taking the AF π with π(MIN) = 1, π(IF_MIN) = 2, π(le) = [ ] and π(add) = [2] together with the lexicographic path order with precedence le ≻ false and le ≻ true, the rules in {7,25} are weakly decreasing and the rules in {5,6,27,28} are strictly decreasing.

Consider the SCC {29,31,32}. The usable rules are {1-4}. By taking the AF π with π(RM) = 2, π(IF_RM) = 3, π(eq) = [ ] and π(add) = [2] together with the lexicographic path order with precedence eq ≻ false and eq ≻ true, the rules in {4,29} are weakly decreasing and the rules in {1-3,31,32} are strictly decreasing.

Consider the SCC {33,36,39}. The usable rules are {1-17}. The constraints could not be solved.

Tyrolean Termination Tool (67.99 seconds) --- May 4, 2006